package model;

import java.util.HashMap;
import java.util.LinkedList;
import java.util.Map;
import model.exceptions.FormulaException;
import model.exceptions.OperatorException;

public class Formula {

    /** 
     * ile znaków na lewo jest pokazywanych przy znalezieniu błedu
     */
    public static final int ERROR_LEFT = 10;
    
    /** 
     * ile znaków na prawo jest pokazywanych przy znalezieniu błedu
     */
    public static final int ERROR_RIGHT = 10;
    
    /**
     * zawiera nowe rzeczy z obecnego węzła
     */
    private String currentNode;
    
    /**
     * formuła z której są tworzone dzieci
     */
    private String formulaToDo;
    /**
     * formuła do pokazania (dodane literały + formuła do tworzenia dzieci)
     */
    private String formulaToShow;
    /**
     * lista formuł do przeanalizowania, pierwszy string to aktualna formuła
     * <br/> ostatnie rzeczy są pierwsze do zrobienia
     */
    private LinkedList<String> todo;
    /**
     * operatory
     */
    private LinkedList<Operator> priorities;
    /**
     * wyłuskane już literały i ich stan
     */
    private HashMap<String, State> literals;
    /**
     * literały dodane przy rozkładzie obecnej formuły
     */
    private HashMap<String, State> newLiterals;
    /**
     * literały i podformuły dodane przy rozkładzie obecnej formuły i ich stan
     * temporalny
     */
    private HashMap<String, Integer> subformulasTemporal;
    /**
     * true jeśli formuła jest OTWARTA: nie ma literału w State.BOTH <br/>
     * false, jeżeli formuła jest DOMKNIĘTA: ma literał w State.BOTH
     */
    private boolean correctness;
    /**
     * znak formuły z której tworzone dzieci
     */
    private boolean signBit;
    /**
     * numer formuły
     */
    private int formulaNumber;
    /**
     * numer rodzica formuły
     */
    private int formulaNumerParent;

    /**
     * do stworzenia root'a drzewa formuł
     *
     * @param _orgFormula
     * @param _signBit
     * @param _priorities
     */
    public Formula(String _formula, boolean _signBit, LinkedList<Operator> _priorities) {
        this.formulaToDo = _formula;
        this.formulaToShow = (_signBit ? "NOT (" : "") + _formula + (_signBit ? ")" : "");
        this.todo = new LinkedList<String>();
        this.literals = new HashMap<String, State>();
        this.newLiterals = new HashMap<String, State>();
        this.subformulasTemporal = new HashMap<String, Integer>();
        this.formulaNumber = 0;
        this.formulaNumerParent = 0;

        this.signBit = _signBit;
        this.priorities = _priorities;

        this.correctness = true;
    }

    /**
     * do tworzenia dzieci w drzewie formuł
     *
     * @param _orgFormula
     * @param newLiterals
     * @param formula
     */
    public Formula(LinkedList<String> _todo, Formula _formula) {
        this.priorities = _formula.getPriorities();
        this.formulaNumerParent = _formula.getFormulaNumber();
        
        this.todo = new LinkedList<String>(_formula.getTodo());
        this.todo.addAll(_todo);
        this.literals = new HashMap<String, State>();
        this.literals.putAll(_formula.getLiterals());
        
        this.newLiterals = new HashMap<String, State>();
        this.subformulasTemporal = new HashMap<String, Integer>();
        
        this.chopFormula();
        this.computeFormulaToShow();
        this.computeCorrectness();
    }

    public LinkedList<Formula> makeChildren() throws OperatorException, FormulaException,
            ArrayIndexOutOfBoundsException {
        LinkedList<Formula> children = new LinkedList<Formula>();

        //System.out.println(this);

        if (this.formulaToDo.equals("")) {
            return children;
        }

        String formula = this.formulaToDo;
        boolean change, found = false;
        do {
            change = false;

            for (Operator oper : this.priorities) {
                //System.out.println("Formula.makeChildern(): oper:" + oper.getSymbol() + ",o.sB:" + oper.getSignBit() + ",f.sB:" + this.signBit);
                
                if (oper.getSignBit() && !this.signBit) {
                    //zabronionym przypadkiem jest kiedy oper.signBit==true && form.signBit==false
                    continue;
                }

                int idx = Formula.getIndexOfOperator(formula, oper.getSymbol());
                if (idx == -1) {
                    continue;
                }
                
                LinkedList<LinkedList<String>> todoLists = oper.decomposite(formula, idx, this.signBit);

                for (LinkedList<String> todoList : todoLists) {
                    children.add(new Formula(todoList, this));
                }

                found = true;
                break;
            }
            
                        if (!found && formula.matches("^\\(.+\\)$")) {
                //System.out.println(formula +"   ---   "+formula.substring(1, formula.length() - 1));
                formula = formula.substring(1, formula.length() - 1);
                change = true;
            }
        } while (!found && change && formula.length() != 0);

        //System.out.println(found+", "+this);

        /**
         * nie znaleziono żadnego operatora - liść!
         */
        if (!found) {
            LinkedList<String> todoList = new LinkedList<String>();
            todoList.add("(" + this.formulaToDo + ");0");
            children.add(new Formula(todoList, this));
        }

        //System.out.println();
        return children;
    }

    /**
     * wkłada literał do mapy
     *
     * @param lit
     */
    private String addLiteral(String _lit) throws ArrayIndexOutOfBoundsException {
        String[] split = _lit.replaceAll("[()]", "").split(";");
        String lit = split[0];
        State state = split[1].equals("0") ? State.TRUE : State.FALSE;
        int temporal;
        try {
            temporal = Integer.valueOf(split[2]);
        } catch (Exception e) {
            temporal = 0;
        }

        // System.out.println("Formula.addLiteral(" + _lit + ") " +
        // this.literals.size() + "|"
        // + this.literals.get(lit));

        if (this.literals.containsKey(lit)) {
            // System.out.println("Formula.addLiteral(" + _lit + ") " +
            // this.literals.get(lit).equals(state));
            if (!this.literals.get(lit).equals(state)) {
                this.literals.put(lit, State.BOTH);
            }
        } else {
            this.literals.put(lit, state);
        }

        this.newLiterals.put(lit, state);
        this.subformulasTemporal.put(lit, temporal);

        return lit;
    }

    /**
     * wyłuskuje literały i wtawia je do mapy, zatrzymuje sie jeśli nie można
     * wyłuskać literału
     *
     * @param _orgFormula
     */
    private void chopFormula() {
        String form;
        this.formulaToDo = "";

        while (!this.todo.isEmpty()) {
            form = this.todo.removeLast();

            // System.out.println("Formula.chopFormula() " + form);

            boolean found = false;
            for (Operator ope : this.priorities) {
                // System.out.println("Formula.chopFormula() "+form + "|" +
                // ope.getSymbol() + "|" + (form.indexOf(ope.getSymbol()) != -1));
                if (form.indexOf(ope.getSymbol()) != -1) {
                    found = true;
                    break;
                }
            }
            if (found) {
                int idx = form.indexOf(';');
                this.formulaToDo = form.substring(0, idx);
                this.signBit = form.substring(idx + 1, idx + 2).equals("1");

                //System.out.println("Prover.chopFormula: formula:"+form+", sB:"+this.signBit);

                int temporal;
                try {
                    temporal = Integer.valueOf(form.substring(idx + 3));
                } catch (Exception e) {
                    temporal = 0;
                }
                this.subformulasTemporal.put(this.formulaToDo, temporal);

                // System.out.println("Formula.chopFormula() "+this.formulaToDo+"|"+this.signBit);

                //znaleziono formułę do przetworzenia
                return;
            } else {
                this.addLiteral(form);
            }
        }
    }

    /**
     *
     * @param value
     * @param signBit
     * @return true jeżeli znak mniejszy od zera
     */
    public static boolean computeSign(String value, boolean signBit) {
        return (value.equals("1") && !signBit) || (value.equals("0") && signBit);
    }

    /**
     * oblicza poprawność formuły na podstawie mapy literałów
     */
    private void computeCorrectness() {
        for (Map.Entry<String, State> lit : this.literals.entrySet()) {
            if (lit.getValue() == State.BOTH) {
                this.correctness = false;
                return;
            }
        }
        this.correctness = true;
    }

    /**
     * zwraca gdzie jest następny zewnętrzny operator, za operator przyjmuje sie
     * dowolny znak ascii nie bedacy literą i nawiasem
     *
     * @param formula
     * @return
     */
    public static int getIndexOfOperator(String formula, String operator) {
        char[] chars = formula.toCharArray();
        // liczba otwartych nawiasów
        int parentheses = 0;
        char cur;

        char[] oper = operator.toCharArray();
        // ile znaków porównano
        int operIdx = 0;

        for (int i = 0; i < chars.length; i++) {
            cur = chars[i];
            if (cur == '(') {
                parentheses++;
                continue;
            }
            if (cur == ')') {
                parentheses--;
                continue;
            }
            if (parentheses == 0) {
                // sprawdź czy pasuje do znaku
                if (cur == oper[operIdx++]) {
                    if (operIdx == oper.length) {
                        return i - operIdx + 1;
                    }
                } else {
                    operIdx = 0;
                }
            }
        }

        return -1;
    }

    public static String deleteParentheses(String formula) throws FormulaException {
        while (formula.matches("^[(].+[)]$")) {
            formula = formula.substring(1, formula.length() - 1);
        }
        if (formula.matches("(^[(].*)|(.*[)]$)")) {
            throw new FormulaException("incorrect parentheses: " + formula);
        }
        return formula;
    }

    private void computeFormulaToShow() {
        this.formulaToShow = (this.signBit ? "NOT": "") +this.formulaToDo;
        for (Map.Entry<String, State> lit : this.literals.entrySet()) {
            String liter = "";
            if (lit.getValue().toString().equals("T")) {
                liter = lit.getKey();
            } else if (lit.getValue().toString().equals("F")) {
                liter = "~" + lit.getKey();
            } else if (lit.getValue().toString().equals("CLOSED")) {
                liter = lit.getKey() + "," + "~" + lit.getKey();
            }
            this.formulaToShow += "," + liter;
        }
        
        //this.formulaToShow = this.formulaToShow.replaceFirst("^,", "");
    }

    /**
     *
     * @return true - formuła NIE zawiera sprzeczności == jest poprawna
     */
    public boolean getCorrectness() {
        return this.correctness;
    }

    public boolean getSignBit() {
        return this.signBit;
    }

    public String getFormulaToDo() {
        return this.formulaToDo;
    }

    public String getFormulaToShow() {
        return this.formulaToShow;
    }

    public LinkedList<String> getTodo() {
        return this.todo;
    }

    public int getTodoSize() {
        return this.todo.size();
    }

    public LinkedList<Operator> getPriorities() {
        return this.priorities;
    }

    public HashMap<String, State> getLiterals() {
        return this.literals;
    }

    public String getLiterslsString() {
        String ret = "";
        for (Map.Entry<String, State> entry : this.literals.entrySet()) {
            String liter = "";
            if (entry.getValue().toString().equals("T")) {
                liter = entry.getKey();
            } else if (entry.getValue().toString().equals("F")) {
                liter = "~" + entry.getKey();
            } else if (entry.getValue().toString().equals("CLOSED")) {
                liter = entry.getKey() + "," + "~" + entry.getKey();
            }
            ret += "," + liter;
        }
        return ret.replaceFirst("^,", "");
    }

    public HashMap<String, State> getNewLiterals() {
        return this.newLiterals;
    }

    public String getNewLiterslsString() {
        String ret = "";
        for (Map.Entry<String, State> entry : this.newLiterals.entrySet()) {
            ret += "," + entry.getKey() + "(" + entry.getValue() + ")";
        }
        return ret.replaceFirst("^,", "");
    }

    public void setPriorities(LinkedList<Operator> _priorities) {
        this.priorities = _priorities;
    }

    protected void setForumlaNumber(int _formulaNumber) {
        this.formulaNumber = _formulaNumber;
    }

    public int getFormulaNumber() {
        return this.formulaNumber;
    }

    public int getFormulaNumberParent() {
        return this.formulaNumerParent;
    }

    /**
     * etykietowanie światów
     *
     * @return
     */
    public String getSubformulasTemporalLabelsWord() {
        String ret = "1";

        for (Map.Entry<String, Integer> entry : this.subformulasTemporal.entrySet()) {
            switch (entry.getValue()) {
                case 0:
                    break;
                case 1:
                    ret += ".[" + entry.getKey() + "]";
                    break;
                case 2:
                    ret += ".(x)";
                    break;
                case 3:
                    // TODO: operator następne
                    break;
            }
        }

        return ret + ":";
    }

    @Override
    public String toString() {
        String ret = ("[" + this.formulaNumber + "," + this.formulaNumerParent + "]") + this.formulaToShow;

        ret += "[closure:" + (this.correctness ? 1 : 0) + "]";
        ret += " lits{" + getLiterslsString() + "}";

        return ret;
    }

    /**
     * prints label for node - in gui
     *
     * @param label - labeling options
     * @return String for node
     */
    public String printMe(int label) {
        //TODO: closed, not closed
        String formula = this.getFormulaToShow();
        String list = " list{" + this.getLiterslsString() + "}";
        switch (label) {
            case 0:
                break;
            case 1:
                formula = "[" + this.formulaNumber + "]" + formula;
                break;
            case 2:
                formula = "[" + this.formulaNumber + "," + this.formulaNumerParent + "]" + formula;
                break;
            //case 3:
            //    formula= this.getSubformulasTemporalLabelsWord()+" "+ formula;
            //    break;
            case 10:
                formula = formula + list;
                break;
            case 11:
                formula = "[" + this.formulaNumber + "]" + formula + list;
                break;
            case 12:
                formula = "[" + this.formulaNumber + "," + this.formulaNumerParent + "]" + formula + list;
                break;
            case 21:
                formula = "[" + this.formulaNumber + "]" + this.getSubformulasTemporalLabelsWord() + " " + formula;
                break;
            case 22:
                formula = "[" + this.formulaNumber + "," + this.formulaNumerParent + "]" + this.getSubformulasTemporalLabelsWord() + " " + formula;
                break;
            case 211:
                formula = "[" + this.formulaNumber + "]" + this.getSubformulasTemporalLabelsWord() + " " + formula + list;
                break;
            case 212:
                formula = "[" + this.formulaNumber + "," + this.formulaNumerParent + "]" + this.getSubformulasTemporalLabelsWord() + " " + formula + list;
                break;

        }
        return formula;
    }

    /**
     * sprawdza poprawność wprowadzonej formuły<br/> - domknięte nawiasy,
     * poprawność operatorów<br/>
     *
     * @param formula do sprawdzenia
     * @param operators lista operatorów
     * @return czy formuła została wpisana prawidłowo true- prawidłowa
     */
    public static boolean validate(String formula, LinkedList<Operator> operators)
            throws FormulaException, Exception {
        //System.out.println("Prover.validate() - start");
        try {
            // sprawdzanie nawiasów
            Formula.checkParentheses(formula);
            //sprawdzanie niepoprawnych znaków
            Formula.checkIncorrectCharacters(formula, operators);
            // sprawdzenie listy operatorów
            Operator.validateList(operators);
            // sprawdzanie użycia operatorów
            Operator.validate(formula, operators);
        } catch (FormulaException fe) {
            System.out.println("Formula.validate() " + fe.getMessage());
            throw fe;
        } catch (Exception e) {
            System.out.println("Formula.validate() " + e.getMessage());
            throw e;
        }

        //System.out.println("Prover.validate() - return true;");
        return true;
    }

    /**
     * funkcja pomocnicza do sprawdzania poprawności nawiasowania <br/ > wyrzuca
     * wyjątek przy błędnym zamknięciu nawiasów
     *
     * @return indeks tablicy
     */
    static public int par(char[] array, int ind, int length) throws FormulaException {

        for (int i = ind; i < length; i++) {
            if (array[i] == ')') {
                if (i == ind) {
                    throw new FormulaException("empty parentheses at index: " + ind);
                } else {
                    return i;
                }
            }
            if (array[i] == '(') {
                i = par(array, ++i, length);
            }
        }
        throw new FormulaException("unclosed parentheses at index: " + ind);
    }

    /**
     * sprawdza poprawność nawiasowania formuły
     *
     * @return poprawne nawiasowanie - true
     */
    static public boolean checkParentheses(String formula) throws FormulaException {
        char[] stringArray = formula.toCharArray();
        int length = stringArray.length;

        for (int ind = 0; ind < length; ind++) {
            char cchar = stringArray[ind];
            if (cchar == '(') {
                ind = par(stringArray, ++ind, length);
            }
            if (cchar == ')') {
                String error = formula.substring(ind, ind+10<formula.length() ? ind+10 : formula.length());
                throw new FormulaException("closing unopened parentheses at index: " + ind + ": "+error);
            }
        }
        // jesli przeszedł całe bez błędów to nawiasy są okej
        return true;
    }

    /**
     * sprawdza czy w formula nie znajdują się niedozowlone znaki
     *
     * @param formula
     * @param operators
     * @return
     * @throws FormulaException
     */
    static public boolean checkIncorrectCharacters(String formula, LinkedList<Operator> operators) throws FormulaException {
        String opeL = Operator.getOperatorsLForRegex(operators);
        String opeB = Operator.getOperatorsBForRegex(operators);
        String opeR = Operator.getOperatorsRForRegex(operators);

        // pusty nawias () - przypadek kiedy sa pod rząd dwa znaki z Operator.availableCharacktersName lub nawiasy
        String incorrenctChars = "^((" + opeL + ")|(" + opeB + ")|(" + opeR + ")|())*$";

        String[] subFormulas = formula.split("[" + Operator.availableCharacktersName + "()]");

        int idx = 0;
        for (String subFormula : subFormulas) {
            if (!subFormula.matches(incorrenctChars)) {
                throw new FormulaException("incorrect characters in formula between index " + idx + " and " + (idx + subFormula.length()));
            }
            idx += subFormula.length() + 1; //+1 za znikający ) lub cyfre
        }

        return true;
    }
}